第2章　PlusCal

TLA+ で仕様を記述する際には、左右を少なくとも 4 つのハイフン（-）で囲まれた MODULE で始まり、少なくとも 4 つの等号（=）で終わる必要がある

MODULE の後にはファイル名と同じモジュール名を指定する

code:tla

---- MODULE wire ----

...

====

インポートしたいモジュールは Extends で指定する

code:tla

EXTENDS Integers

1 行コメントは \*、ブロックコメントは (* ... *) で表す

式はすべて {TRUE} のような値か、+ のような演算子のどちらか

PlusCal で仕様を記述する際には、Parser に無視されるようにコメント内に記述する

具体的には、--algorithm <アルゴリズム名> ~ end algorithm 内に記述する

アルゴリズム名はモジュール名と同じく、ファイル名を指定する

code:tla

(*--algorithm wire

...

end algorithm;*)

アルゴリズム内部では variables を使って変数を初期化する

変数は , または ; で区切る

code:tla

variables

people = {"alice", "bob"},

acc = p \in people |-> 5,

TLA+ では基本的な値として文字列と整数、ブール値、モデル値の 4 種類がある

論理演算子をサポート

等しい: x = y

等しくない: x /= y or x # y

論理積（AND）: x /\ y

論理和（OR）: x \/ y

代入: x := y

否定（NOT）: "x

Integers モジュールを使うと、算術演算も実行できる: +、-、%、*

除算は \div で、小数の演算はサポートしていない

範囲演算子 .. もサポート

TLA+ では集合、タプル（シーケンス）、構造体、関数の 4 種類の型がある

集合: {"a", "b", "c"}

サポートされている演算子

x \in set: x が集合 set に含まれるか

x \notin set: x が集合 set に含まれていないか

set1 \subseteq set2: set1 は set2 の部分集合か

set1 \union set2: 和集合

\cup でも可能

set1 \intersect set2: 積集合

\cap でも可能

set1 \ set2: 差集合

Cardinality(set): 集合 set 内の要素の個数（warning.icon FiniteSets モジュールが必要）

フィルタリングするには {x \in set: <条件式>}

マッピングするには {<式>: \x in set}

タプル: <<"a", {1, 2}>>

...